| Definitions |  , if p:P then A(p) else B fi , null(as),  b, if nms1 and nms2 overlap then x else y fi, Rtransform(f;A), R|names,  T, R-names(A), Rsends-T(x1), Rsends-knd(x1), Reffect-T(x1), f(x)?z, p   q, Reffect-knd(x1), let x = a in b(x), Reffect?(x1),  x:A. B(x), A c B, Rsends-dt(x1), Rsends-l(x1), Rsends?(x1), R-interface-compat(A;B), (x  l), Realizer, SQType(T),   x. t(x), f || g, P   Q, P  Q, S  T, Top, True, P  Q,  xL. P(x), A B, MaName, {T}, Rplus-right(x1), Rplus-left(x1), P & Q, ff, tt, if b then t else f fi , i  j , False,  A, A  B, Y,  , t T, A || B, P Q, x:A. B(x), x(s), l_disjoint(T;l1;l2), Dec(P), Unit,  ,  , Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),  , fpf-domain(f) |
| Lemmas | bool sq, bool cases, l disjoint intersection implies2, top wf, l disjoint intersection implies, l disjoint wf, decidable wf, IdLnk sq, pi1 wf, remove-repeats wf, lsrc wf, isrcv wf, true wf, squash wf, Knd sq, isrcv-implies, rcv wf, ldst wf, locknd functionality isrcv, member-remove-repeats, member-fpf-dom, decidable equal Id, decidable l member, cons member, member map, fpf-domain wf, map wf, assert-eq-lnk, tagof wf, Rsends wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, append wf, nil member, and functionality wrt iff, length wf1, select wf, length wf2, false wf, all functionality wrt iff, finite-prob-space wf, decl-type wf, decl-state wf, IdLnk wf, rationals wf, unit wf, R-discrete-compat-disjoint-names, R-frame-compat-disjoint-names, R-base-domain-common-name, assert-eq-bd, R-base-domain wf, eq bd wf, Rda-R-names, locknd wf, Id sq, Rds-R-names, Rda wf, Kind-deq wf, Knd wf, fpf wf, fpf-trivial-subtype-top, Rds wf, id-deq wf, fpf-dom wf, not functionality wrt iff, assert-eq-id, R-loc wf, eq id wf, disjoint-iff-null-intersection, assert of null, null wf3, decidable assert, Rnone? wf, R-sub-self, R-sub-plus-right, Id wf, LocKnd wf, member append, member-intersection, l member wf, implies functionality wrt iff, Rplus-right wf, R-sub-plus-left, Rplus-implies, R-restrict functionality, R-compat-sub, Rplus-left wf, R-size-decreases, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, ge wf, nat properties, not wf, bnot wf, assert wf, bool wf, Rplus? wf, es realizer wf, nat plus wf, le wf, R-names wf, maname-deq wf, MaName wf, l intersection wf, R-restrict wf, R-compat wf, R-size wf, nat wf |